\documentclass{article}
\usepackage{amsmath}

\begin{document}
\textbf{Name: Mathias Andersen} \\
\textbf{Group: d502e11} \\
\textbf{Semester: DAT5}\\
\textbf{Subject:  Revised answer for problem 3.2, Lambda Calculus Hand In.}
\\
\\

Problem 3.2. Apply the $W$-algorithm to the expression $e$ given by $let f=\lambda x.\lambda g.g(x) in f 484$.
Let $e_1=\lambda x.\lambda g.g(x)$ and $e_2=f 484$. \\
$W(E_{\emptyset},e)=(\sigma_2 \circ \sigma_1,s_2)$, where 
$$W(E_{\emptyset},e_1)=(\sigma_1,s_1)$$ and $E'=\sigma_1(E_{\emptyset})[f\mapsto close(\sigma_1(E_{\emptyset});s_1)]$ and $$W(E',e_2)=(\sigma_2,s_2).$$

We now find $W(E_{\emptyset},e_1)$: \\

$W(E_{\emptyset},e_1)=(\sigma_3,\sigma_3(a)\rightarrow t)$, where $W(E_{\emptyset}[x\mapsto a],\lambda g.g(x))=(\sigma_3,t)$. Now

$$W(E_{\emptyset}[x\mapsto a],\lambda g.g(x))=(\sigma_4,\sigma_4(b) \rightarrow t_2),$$ 

where $W(E_{\emptyset}[x\mapsto a,g\mapsto b],g(x))=(\sigma_4,t_2)$. To find $W(E_{\emptyset}[x\mapsto a,g\mapsto b],g(x))$ we calculate:

$$W(E_{\emptyset}[x\mapsto a,g\mapsto b],g)=(id,b)$$ and 

$$W(E_{\emptyset}[x\mapsto a,g\mapsto b],x)=(id,a).$$

The most general unifier for $b$ and $a \rightarrow c$ is $\sigma_g=[b\mapsto (a \rightarrow c)]$.

We now know that 

$$W(E_{\emptyset}[x\mapsto a,g\mapsto b],g(x))=(\sigma_g\circ id \circ id,\sigma_g c)=(\sigma_g,c),$$

and we can conlude that $\sigma_4=\sigma_g$ and $t_2=c$. These values can be inserted above, and we thus get $W(E_{\emptyset}[x\mapsto a],\lambda g.g(x))=(\sigma_g,a\rightarrow c \rightarrow c)$. Which gives us
$$W(E_{\emptyset},e_1)=(\sigma_g,a\rightarrow a\rightarrow c \rightarrow c),$$ and these values can be substituted for $\sigma_1$ and $s_1$ above. \\

We can now conclude that $E'=E_{\emptyset}[f\mapsto a\rightarrow a\rightarrow c \rightarrow c]$ and to calculate 
$$W(E',e_2)=W(E_{\emptyset}[f\mapsto a\rightarrow a\rightarrow c \rightarrow c],f 484),$$
 we compute:
$$W(E_{\emptyset}[f\mapsto a\rightarrow a\rightarrow c \rightarrow c],f)=(id,a\rightarrow a\rightarrow c \rightarrow c)$$ and 
$$W(E_{\emptyset}[f\mapsto a\rightarrow a\rightarrow c \rightarrow c],484)=(id,Int)$$ 
Now we must find a most general unifier for the two types 
$a\rightarrow a\rightarrow c \rightarrow c$ and  $Int \rightarrow d$. Since this unifier cannot be found the algorithm fails, and the type of $e$ can not be inferred. 

\end{document}
